‚ 計算 | 補遺 ソフトウェア基礎論配布資料単純型付

ソフトウェア基礎論配布資料 単純型付

計算

補遺

五十嵐 淳

京都大学 大学院情報学研究科知能情報学専攻

平成

年

月

日

4

諸性質

4.1 定理 [Uniquness of Typing]: Γ`t:T かつ Γ`t:T⁰ ならばT ≡T⁰ である．

4.2 定理 [Type Preservation]: Γ`t:T かつ t−→<sup>v</sup> t<sup>0</sup> ならば，Γ`t⁰:T である．

4.3 定理 [Progress]: • `t:T ならば tは値であるか，ある項 t⁰が存在してt−→v t⁰ である．

4.4 定理 [Normalization]: Γ ` t:T かつ t が fix を含まないならば t −→v t₁ −→v · · · −→v

t_n−→v· · · なる無限列は存在しない．

5 Type Preservation

と

の略証

5.1 Lemma [Inversion]: 1. もし Γ`λx:T<sub>1</sub>.t<sub>0</sub> :T ならば，T<sub>1</sub>, T<sub>2</sub> が存在してT ≡T<sub>1</sub>→T<sub>2</sub> か つΓ, x:T<sub>1</sub> `t₀:T₂ が成立する．

2. もし Γ`t1 t2 :T ならば，T1 が存在してΓ`t1:T1→T かつ Γ`t2 :T1 が成立する．

3. もし Γ`if t1 then t2 else t3 :T ならば，Γ`t1 :bool かつ Γ`t2 :T かつ Γ`t3 :T などなど．

Proof: (変数参照項を除いて)項について適用できる型付け規則がひとつなので，型付け規則を逆

(下から上)に読むことによって明らか． ¤

5.2 Lemma [Substitution Preserves Typing]: Γ, x : T⁰ ` t : T かつ Γ ` t⁰ : T⁰ ならばΓ ` [x7→t⁰]t:T が成立する．

Proof: [x7→t⁰]t≡ ⇓x([(⇑xt⁰)/x]t) に注意すると，以下の三つを示せばよい，

• Γ`t:T ならば Γ, x:T<sup>0</sup> ` ⇑^xt:T

1

• Γ, x:T⁰ `t:T かつ x6∈F V(t) ならばΓ` ⇓xt:T

• Γ, x:T⁰ `t:T かつ Γ, x:T<sup>0</sup> `t⁰ :T⁰ ならば Γ, x:T⁰ `[t⁰/x]t:T かつ x6∈F V([t⁰/x]t) 最初の二つは，項の構成に関する帰納法で証明できる．最後のものは，命題をもう少し一般化してか

ら，型付け関係の導出に関する帰納法で証明できる． ¤

Proof of Type Preservation: t−→v t⁰ の導出に関する帰納法で証明する．帰納法のbase に相 当するのはEv-AbsApp ^{など前提のない規則で} t−→v t⁰ が導出された場合である．

• ^規則 Ev-AbsApp ^{の場合，ある}x, T⁰, t0, v2 が存在してt≡(λx:T⁰.t0)v2 かつt⁰ ≡[x7→v2]t0

である．Inversionより，Γ, x:T⁰ `t<sub>0</sub> :T かつ Γ`v₂:T⁰ が成立する．Substitution Preserves Typing よりΓ`[x7→v<sub>2</sub>]t<sub>1</sub>:T つまりΓ`t⁰:T である．

• ^規則 Ev-FixAbs ^の場合，. . .

• ^規則 Ev-PlusZero の場合，. . .

• ^{などなど．}

帰納法のステップに相当するのは，前提のある規則でt−→v t⁰ が導出された場合である．この時，

前提として成立しているt0 −→^v t⁰₀ に関してはType Preservation が成立しているとしてよい(帰納 法の仮定)．

• ^規則 Ev-App1^{の場合，ある} t1, t2, t⁰₁ が存在してt≡t1t2 かつ t⁰≡t⁰₁t2 かつt1 −→^v t⁰₁ が成 立する．Inversionより，あるT₁ が存在してΓ`t<sub>1</sub> :T<sub>1</sub> →T かつΓ`t₂ :T₁ である．帰納法 の仮定よりΓ`t<sup>0</sup><sub>1</sub>:T<sub>1</sub> →T が成立する．T-App<sup>より</sup>Γ`t⁰₁t₂ :T が導出できる．

• ^{などなど．} ¤

5.3 Lemma [Canonical Forms]: 1. もし • ` v :T₁ → T₂ ならば，ある x, T₁, t₀ が存在して v≡λx:T₁.t₀ が成立する．

2. もし • `v:natならば，v≡0またはあるnが存在してS(n)が成立する．

3. もし • `v:boolならば， v≡true またはv≡false

Proof of Progress: 型付け関係• `t:T に関する帰納法で証明する．tの形で場合分けを行なう．

• t≡#ⁿx の場合はあり得ない．

• t≡λx:T.t0 の場合，tは値である．

• t≡t₁ t₂ の場合，Inversion より，あるT₁ が存在して• `t<sub>1</sub> :T<sub>1</sub> →T かつ• `t₂ :T₁ が成立 する．帰納法の仮定よりt₁ が値であるか，あるt⁰₁ が存在してt₁ −→v t⁰₁ である．前者の場合，

Canonical Forms よりt₁ ≡λx:T₁.t₀ であるので，Ev-AbsApp ^よりt₁ t₂ −→v [x 7→ t₂]t₀ を 導出することができる．一方，後者の場合，Ev-App1 ^よりt1 t2−→v t⁰₁ t2 を導出することが でき，結局t−→v t⁰ なる t⁰ が存在する．

• ^{などなど．} ¤

2